felix.git/test/golden/inductive/generating tasks.golden, branch hotg Unnamed repository; edit this file 'description' to name the repository. https://git.adelon.net/felix.git/atom?h=hotg 2026-08-03T19:00:28+00:00 Remove obsolete verification machinery 2026-08-03T19:00:28+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-03T19:00:28+00:00 urn:sha1:5cdde1fd0f976863ae4b5831ab389048138b06a4 Check direct inductives through fixed-point replay 2026-07-28T12:54:42+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T12:54:42+00:00 urn:sha1:ba4acdaa305d01469f66cd316edde4d22ea2fff9 Validate relation parameter arity 2026-07-27T16:19:29+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-27T15:32:47+00:00 urn:sha1:3b573d94d4c5e82802745daa7c7d679727155e7d Use semantic subset formula inside inductive defns 2026-07-23T17:56:52+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-23T17:56:52+00:00 urn:sha1:d1d3f178db000a6ffd928a75af8eb1ba2b7f8b9a Track ownership of top-level symbols 2026-07-03T00:13:21+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-03T00:13:21+00:00 urn:sha1:40bc466d6a996e731cba21f24a58be08b1f22689 Require every ownable top-level symbol to be introduced by a dedicated owner before it can appear in facts. Reject duplicate ownership and prevent symbols used by inductive definitions from being defined later. Use the ownership/dependency information to reject hidden recursive inductive definitions and to generate referenceable inductive principles. BREAKING CHANGE: Top-level facts no longer introduce symbols implicitly. Use shorter `_local_N` marker in TPTP output 2026-02-24T15:15:26+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-02-24T15:15:26+00:00 urn:sha1:330fa14bf6f075342cbe8e515d67740fd1edcf00 Update golden tests 2026-02-13T23:54:25+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-02-13T23:54:25+00:00 urn:sha1:1122576d9283d499915ec4d0a87ee8cf03e5339e Use tries for patterns, skip trivial hypotheses 2026-02-06T01:26:17+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-02-06T01:26:17+00:00 urn:sha1:8a6e8d455048b2510e25af943785241752c29b9c Cache encoding of hypotheses 2026-02-05T20:03:20+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-02-05T20:03:20+00:00 urn:sha1:54ae3e3d02af5e26e1f92f2a3766ac85e8116294 Remove `lookupLexicalItem`, attach info in AST instead 2026-02-05T18:50:34+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-02-05T18:50:34+00:00 urn:sha1:b25ec4c14cc4c4cfc0dd410a4b8cd74d411ad06c